<html>
<head><meta charset="utf-8"><title>Rust verification tools · wg-secure-code · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/index.html">wg-secure-code</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/Rust.20verification.20tools.html">Rust verification tools</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="209259487"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/Rust%20verification%20tools/near/209259487" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alastair Reid <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/Rust.20verification.20tools.html#209259487">(Sep 07 2020 at 05:51)</a>:</h4>
<p>[crossposted from wg-formal-methods]</p>
<p>My team in Google Research has been thinking about what we want in Rust verification.<br>
We want to narrow the gap between testing and verification. e.g., by making it easy to switch back and forth between testing and verification.</p>
<p>So we have been reimplementing the proptest library so that you can use the same test harness for testing/fuzzing with proptest and for formal verification using automatic verification tools like KLEE.</p>
<p>It's early days yet but we have something that works and we would love feedback on whether this is a direction that the community should go in or not.</p>
<p>Code: <a href="https://github.com/project-oak/rust-verification-tools">https://github.com/project-oak/rust-verification-tools</a><br>
Blog post: <a href="https://alastairreid.github.io/why-not-both/">https://alastairreid.github.io/why-not-both/</a><br>
Tweet: <a href="https://twitter.com/alastair_d_reid/status/1301543693233655810">https://twitter.com/alastair_d_reid/status/1301543693233655810</a></p>
<div class="inline-preview-twitter"><div class="twitter-tweet"><a href="https://twitter.com/alastair_d_reid/status/1301543693233655810"><img class="twitter-avatar" src="https://pbs.twimg.com/profile_images/731458319433519104/q1EULfSQ_normal.jpg"></a><p>Verifying vs testing?  Why not both?
New blog post about our work on Rust verification based on reimplementing the proptest library for formal verification tools so you can use the same test harness with both proptest and with “propverify”.
<a href="https://twitter.com/rustlang">@rustlang</a> #KLEE
<a href="https://t.co/rAzAvW6MCI">https://alastairreid.github.io/why-not-both/</a></p><span>- Alastair Reid (@alastair_d_reid)</span></div></div>



<a name="209286220"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/Rust%20verification%20tools/near/209286220" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Joshua Nelson <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/Rust.20verification.20tools.html#209286220">(Sep 07 2020 at 11:42)</a>:</h4>
<p>I would be very interested in this! A related area that's bugged me is that each of the fuzzing libraries needs a slightly different test harness, so you end up writing practically the same code several times. It would be great to have a 'shared vocabulary' that lets you use the same code for each</p>



<a name="209286273"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/Rust%20verification%20tools/near/209286273" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Joshua Nelson <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/Rust.20verification.20tools.html#209286273">(Sep 07 2020 at 11:43)</a>:</h4>
<p>See <a href="https://github.com/jyn514/saltwater/tree/master/fuzz">https://github.com/jyn514/saltwater/tree/master/fuzz</a> for an example of what I mean</p>



<a name="209411532"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/Rust%20verification%20tools/near/209411532" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Tony Arcieri <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/Rust.20verification.20tools.html#209411532">(Sep 08 2020 at 16:31)</a>:</h4>
<p><span class="user-mention" data-user-id="336739">@Alastair Reid</span> I saw that... looks amazing!</p>



<a name="209411783"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/Rust%20verification%20tools/near/209411783" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Tony Arcieri <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/Rust.20verification.20tools.html#209411783">(Sep 08 2020 at 16:33)</a>:</h4>
<p><span class="user-mention" data-user-id="336739">@Alastair Reid</span> I've played with some sort of similar symbolic execution tools from Galois (mir-verifier/crux-mir, backed by yices), but having a common interface for proptest and symbolic execution tooling is pretty amazing</p>



<a name="209411831"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/Rust%20verification%20tools/near/209411831" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Tony Arcieri <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/Rust.20verification.20tools.html#209411831">(Sep 08 2020 at 16:33)</a>:</h4>
<p>we use proptest quite a bit in RustCrypto</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>